The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

map(Cons(x, xs)) → Cons(f(x), map(xs))
map(Nil) → Nil
goal(xs) → map(xs)
f(x) → *(x, x)
+Full(S(x), y) → +Full(x, S(y))
+Full(0, y) → y

The (relative) TRS S consists of the following rules:

*(x, S(S(y))) → +(x, *(x, S(y)))
*(x, S(0)) → x
*(x, 0) → 0
*(0, y) → 0

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

map(Cons(x, xs)) → Cons(f(x), map(xs))
map(Nil) → Nil
goal(xs) → map(xs)
f(x) → *'(x, x)
+Full(S(x), y) → +Full(x, S(y))
+Full(0', y) → y

The (relative) TRS S consists of the following rules:

*'(x, S(S(y))) → +'(x, *'(x, S(y)))
*'(x, S(0')) → x
*'(x, 0') → 0'
*'(0', y) → 0'

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Innermost TRS:
Rules:
map(Cons(x, xs)) → Cons(f(x), map(xs))
map(Nil) → Nil
goal(xs) → map(xs)
f(x) → *'(x, x)
+Full(S(x), y) → +Full(x, S(y))
+Full(0', y) → y
*'(x, S(S(y))) → +'(x, *'(x, S(y)))
*'(x, S(0')) → x
*'(x, 0') → 0'
*'(0', y) → 0'

Types:
map :: Cons:Nil → Cons:Nil
Cons :: S:0':+' → Cons:Nil → Cons:Nil
f :: S:0':+' → S:0':+'
Nil :: Cons:Nil
goal :: Cons:Nil → Cons:Nil
*' :: S:0':+' → S:0':+' → S:0':+'
+Full :: S:0':+' → S:0':+' → S:0':+'
S :: S:0':+' → S:0':+'
0' :: S:0':+'
+' :: S:0':+' → S:0':+' → S:0':+'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0':+'2_0 :: S:0':+'
gen_Cons:Nil3_0 :: Nat → Cons:Nil
gen_S:0':+'4_0 :: Nat → S:0':+'

(5) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
map, *', +Full

(6) Obligation:

Innermost TRS:
Rules:
map(Cons(x, xs)) → Cons(f(x), map(xs))
map(Nil) → Nil
goal(xs) → map(xs)
f(x) → *'(x, x)
+Full(S(x), y) → +Full(x, S(y))
+Full(0', y) → y
*'(x, S(S(y))) → +'(x, *'(x, S(y)))
*'(x, S(0')) → x
*'(x, 0') → 0'
*'(0', y) → 0'

Types:
map :: Cons:Nil → Cons:Nil
Cons :: S:0':+' → Cons:Nil → Cons:Nil
f :: S:0':+' → S:0':+'
Nil :: Cons:Nil
goal :: Cons:Nil → Cons:Nil
*' :: S:0':+' → S:0':+' → S:0':+'
+Full :: S:0':+' → S:0':+' → S:0':+'
S :: S:0':+' → S:0':+'
0' :: S:0':+'
+' :: S:0':+' → S:0':+' → S:0':+'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0':+'2_0 :: S:0':+'
gen_Cons:Nil3_0 :: Nat → Cons:Nil
gen_S:0':+'4_0 :: Nat → S:0':+'

Generator Equations:
gen_Cons:Nil3_0(0) ⇔ Nil
gen_Cons:Nil3_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil3_0(x))
gen_S:0':+'4_0(0) ⇔ 0'
gen_S:0':+'4_0(+(x, 1)) ⇔ S(gen_S:0':+'4_0(x))

The following defined symbols remain to be analysed:
map, *', +Full

(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
map(gen_Cons:Nil3_0(n6_0)) → gen_Cons:Nil3_0(n6_0), rt ∈ Ω(1 + n6₀)

Induction Base:
map(gen_Cons:Nil3_0(0)) →_R^Ω(1)
Nil

Induction Step:
map(gen_Cons:Nil3_0(+(n6_0, 1))) →_R^Ω(1)
Cons(f(0'), map(gen_Cons:Nil3_0(n6_0))) →_R^Ω(1)
Cons(*'(0', 0'), map(gen_Cons:Nil3_0(n6_0))) →_R^Ω(0)
Cons(0', map(gen_Cons:Nil3_0(n6_0))) →_IH
Cons(0', gen_Cons:Nil3_0(c7_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(8) Complex Obligation (BEST)

(9) Obligation:

Innermost TRS:
Rules:
map(Cons(x, xs)) → Cons(f(x), map(xs))
map(Nil) → Nil
goal(xs) → map(xs)
f(x) → *'(x, x)
+Full(S(x), y) → +Full(x, S(y))
+Full(0', y) → y
*'(x, S(S(y))) → +'(x, *'(x, S(y)))
*'(x, S(0')) → x
*'(x, 0') → 0'
*'(0', y) → 0'

Types:
map :: Cons:Nil → Cons:Nil
Cons :: S:0':+' → Cons:Nil → Cons:Nil
f :: S:0':+' → S:0':+'
Nil :: Cons:Nil
goal :: Cons:Nil → Cons:Nil
*' :: S:0':+' → S:0':+' → S:0':+'
+Full :: S:0':+' → S:0':+' → S:0':+'
S :: S:0':+' → S:0':+'
0' :: S:0':+'
+' :: S:0':+' → S:0':+' → S:0':+'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0':+'2_0 :: S:0':+'
gen_Cons:Nil3_0 :: Nat → Cons:Nil
gen_S:0':+'4_0 :: Nat → S:0':+'

Lemmas:
map(gen_Cons:Nil3_0(n6_0)) → gen_Cons:Nil3_0(n6_0), rt ∈ Ω(1 + n6₀)

Generator Equations:
gen_Cons:Nil3_0(0) ⇔ Nil
gen_Cons:Nil3_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil3_0(x))
gen_S:0':+'4_0(0) ⇔ 0'
gen_S:0':+'4_0(+(x, 1)) ⇔ S(gen_S:0':+'4_0(x))

The following defined symbols remain to be analysed:
*', +Full

(10) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol *'.

(11) Obligation:

Innermost TRS:
Rules:
map(Cons(x, xs)) → Cons(f(x), map(xs))
map(Nil) → Nil
goal(xs) → map(xs)
f(x) → *'(x, x)
+Full(S(x), y) → +Full(x, S(y))
+Full(0', y) → y
*'(x, S(S(y))) → +'(x, *'(x, S(y)))
*'(x, S(0')) → x
*'(x, 0') → 0'
*'(0', y) → 0'

Types:
map :: Cons:Nil → Cons:Nil
Cons :: S:0':+' → Cons:Nil → Cons:Nil
f :: S:0':+' → S:0':+'
Nil :: Cons:Nil
goal :: Cons:Nil → Cons:Nil
*' :: S:0':+' → S:0':+' → S:0':+'
+Full :: S:0':+' → S:0':+' → S:0':+'
S :: S:0':+' → S:0':+'
0' :: S:0':+'
+' :: S:0':+' → S:0':+' → S:0':+'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0':+'2_0 :: S:0':+'
gen_Cons:Nil3_0 :: Nat → Cons:Nil
gen_S:0':+'4_0 :: Nat → S:0':+'

Lemmas:
map(gen_Cons:Nil3_0(n6_0)) → gen_Cons:Nil3_0(n6_0), rt ∈ Ω(1 + n6₀)

Generator Equations:
gen_Cons:Nil3_0(0) ⇔ Nil
gen_Cons:Nil3_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil3_0(x))
gen_S:0':+'4_0(0) ⇔ 0'
gen_S:0':+'4_0(+(x, 1)) ⇔ S(gen_S:0':+'4_0(x))

The following defined symbols remain to be analysed:
+Full

(12) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
+Full(gen_S:0':+'4_0(n89193_0), gen_S:0':+'4_0(b)) → gen_S:0':+'4_0(+(n89193_0, b)), rt ∈ Ω(1 + n89193₀)

Induction Base:
+Full(gen_S:0':+'4_0(0), gen_S:0':+'4_0(b)) →_R^Ω(1)
gen_S:0':+'4_0(b)

Induction Step:
+Full(gen_S:0':+'4_0(+(n89193_0, 1)), gen_S:0':+'4_0(b)) →_R^Ω(1)
+Full(gen_S:0':+'4_0(n89193_0), S(gen_S:0':+'4_0(b))) →_IH
gen_S:0':+'4_0(+(+(b, 1), c89194_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(13) Complex Obligation (BEST)

(14) Obligation:

Innermost TRS:
Rules:
map(Cons(x, xs)) → Cons(f(x), map(xs))
map(Nil) → Nil
goal(xs) → map(xs)
f(x) → *'(x, x)
+Full(S(x), y) → +Full(x, S(y))
+Full(0', y) → y
*'(x, S(S(y))) → +'(x, *'(x, S(y)))
*'(x, S(0')) → x
*'(x, 0') → 0'
*'(0', y) → 0'

Types:
map :: Cons:Nil → Cons:Nil
Cons :: S:0':+' → Cons:Nil → Cons:Nil
f :: S:0':+' → S:0':+'
Nil :: Cons:Nil
goal :: Cons:Nil → Cons:Nil
*' :: S:0':+' → S:0':+' → S:0':+'
+Full :: S:0':+' → S:0':+' → S:0':+'
S :: S:0':+' → S:0':+'
0' :: S:0':+'
+' :: S:0':+' → S:0':+' → S:0':+'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0':+'2_0 :: S:0':+'
gen_Cons:Nil3_0 :: Nat → Cons:Nil
gen_S:0':+'4_0 :: Nat → S:0':+'

Lemmas:
map(gen_Cons:Nil3_0(n6_0)) → gen_Cons:Nil3_0(n6_0), rt ∈ Ω(1 + n6₀)
+Full(gen_S:0':+'4_0(n89193_0), gen_S:0':+'4_0(b)) → gen_S:0':+'4_0(+(n89193_0, b)), rt ∈ Ω(1 + n89193₀)

Generator Equations:
gen_Cons:Nil3_0(0) ⇔ Nil
gen_Cons:Nil3_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil3_0(x))
gen_S:0':+'4_0(0) ⇔ 0'
gen_S:0':+'4_0(+(x, 1)) ⇔ S(gen_S:0':+'4_0(x))

No more defined symbols left to analyse.

(15) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
map(gen_Cons:Nil3_0(n6_0)) → gen_Cons:Nil3_0(n6_0), rt ∈ Ω(1 + n6₀)

(16) BOUNDS(n^1, INF)

(17) Obligation:

Innermost TRS:
Rules:
map(Cons(x, xs)) → Cons(f(x), map(xs))
map(Nil) → Nil
goal(xs) → map(xs)
f(x) → *'(x, x)
+Full(S(x), y) → +Full(x, S(y))
+Full(0', y) → y
*'(x, S(S(y))) → +'(x, *'(x, S(y)))
*'(x, S(0')) → x
*'(x, 0') → 0'
*'(0', y) → 0'

Types:
map :: Cons:Nil → Cons:Nil
Cons :: S:0':+' → Cons:Nil → Cons:Nil
f :: S:0':+' → S:0':+'
Nil :: Cons:Nil
goal :: Cons:Nil → Cons:Nil
*' :: S:0':+' → S:0':+' → S:0':+'
+Full :: S:0':+' → S:0':+' → S:0':+'
S :: S:0':+' → S:0':+'
0' :: S:0':+'
+' :: S:0':+' → S:0':+' → S:0':+'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0':+'2_0 :: S:0':+'
gen_Cons:Nil3_0 :: Nat → Cons:Nil
gen_S:0':+'4_0 :: Nat → S:0':+'

Lemmas:
map(gen_Cons:Nil3_0(n6_0)) → gen_Cons:Nil3_0(n6_0), rt ∈ Ω(1 + n6₀)
+Full(gen_S:0':+'4_0(n89193_0), gen_S:0':+'4_0(b)) → gen_S:0':+'4_0(+(n89193_0, b)), rt ∈ Ω(1 + n89193₀)

Generator Equations:
gen_Cons:Nil3_0(0) ⇔ Nil
gen_Cons:Nil3_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil3_0(x))
gen_S:0':+'4_0(0) ⇔ 0'
gen_S:0':+'4_0(+(x, 1)) ⇔ S(gen_S:0':+'4_0(x))

No more defined symbols left to analyse.

(18) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
map(gen_Cons:Nil3_0(n6_0)) → gen_Cons:Nil3_0(n6_0), rt ∈ Ω(1 + n6₀)

(19) BOUNDS(n^1, INF)

(20) Obligation:

Innermost TRS:
Rules:
map(Cons(x, xs)) → Cons(f(x), map(xs))
map(Nil) → Nil
goal(xs) → map(xs)
f(x) → *'(x, x)
+Full(S(x), y) → +Full(x, S(y))
+Full(0', y) → y
*'(x, S(S(y))) → +'(x, *'(x, S(y)))
*'(x, S(0')) → x
*'(x, 0') → 0'
*'(0', y) → 0'

Types:
map :: Cons:Nil → Cons:Nil
Cons :: S:0':+' → Cons:Nil → Cons:Nil
f :: S:0':+' → S:0':+'
Nil :: Cons:Nil
goal :: Cons:Nil → Cons:Nil
*' :: S:0':+' → S:0':+' → S:0':+'
+Full :: S:0':+' → S:0':+' → S:0':+'
S :: S:0':+' → S:0':+'
0' :: S:0':+'
+' :: S:0':+' → S:0':+' → S:0':+'
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0':+'2_0 :: S:0':+'
gen_Cons:Nil3_0 :: Nat → Cons:Nil
gen_S:0':+'4_0 :: Nat → S:0':+'

Lemmas:
map(gen_Cons:Nil3_0(n6_0)) → gen_Cons:Nil3_0(n6_0), rt ∈ Ω(1 + n6₀)

Generator Equations:
gen_Cons:Nil3_0(0) ⇔ Nil
gen_Cons:Nil3_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil3_0(x))
gen_S:0':+'4_0(0) ⇔ 0'
gen_S:0':+'4_0(+(x, 1)) ⇔ S(gen_S:0':+'4_0(x))

No more defined symbols left to analyse.

(21) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
map(gen_Cons:Nil3_0(n6_0)) → gen_Cons:Nil3_0(n6_0), rt ∈ Ω(1 + n6₀)

(22) BOUNDS(n^1, INF)